p:PosetSig, a, b:|p|. ((a < b)) = (a <p b)   

latex

Up	sets 1
Definitions of Statement	a <p b
Definitions	t  T, a <p b, , x:A. B(x)
Lemmas	poset sig wf, set car wf, set blt wf, assert wf